\begin{tabbing}
weak{-}precond{-}send{-}p(${\it es}$;$T$;$A$;$l$;${\it tg}$;$a$;${\it ds}$;$P$;$f$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=($\forall$$x$:Id. es{-}vartype(${\it es}$; source($l$); $x$) $\subseteq\rho$ fpf{-}cap(${\it ds}$;IdDeq;$x$;Top))\+
\\[0ex]\& alle{-}at(${\it es}$;source($l$);$e$.es{-}kind(${\it es}$; $e$) $=$ locl($a$) $\in$ Knd $\Rightarrow$ es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $A$)
\\[0ex]\& ($\forall$$e$:es{-}E(${\it es}$). es{-}kind(${\it es}$; $e$) $=$ rcv($l$,${\it tg}$) $\in$ Knd $\Rightarrow$ es{-}valtype(${\it es}$; $e$) $\subseteq\rho$ $T$)
\\[0ex]\& \=(\=$\forall$${\it e'}$:es{-}E(${\it es}$).\+\+
\\[0ex]es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd
\\[0ex]$\Rightarrow$ \=es{-}kind(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)) $=$ locl($a$) $\in$ Knd\+
\\[0ex]\& \=$P$(es{-}state{-}when(${\it es}$;es{-}sender(${\it es}$; ${\it e'}$)),es{-}val(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)))\+
\\[0ex]\& \=es{-}val(${\it es}$; ${\it e'}$)\+
\\[0ex]$=$
\\[0ex]$f$(es{-}state{-}when(${\it es}$;es{-}sender(${\it es}$; ${\it e'}$)),es{-}val(${\it es}$; es{-}sender(${\it es}$; ${\it e'}$)))
\\[0ex]$\in$ $T$)
\-\-\-\-\\[0ex]\& \=alle{-}at(${\it es}$;source($l$);$e$.$\exists$${\it e'}$:es{-}E(${\it es}$).\+
\\[0ex]es{-}causle(${\it es}$;$e$;${\it e'}$)
\\[0ex]\& \=es{-}kind(${\it es}$; ${\it e'}$) $=$ rcv($l$,${\it tg}$) $\in$ Knd \& es{-}le(${\it es}$;$e$;es{-}sender(${\it es}$; ${\it e'}$))\+
\\[0ex]$\vee$ es{-}loc(${\it es}$; ${\it e'}$) $=$ source($l$) $\in$ Id \& ($\forall$$v$:$A$. $\neg$$P$(es{-}state{-}after(${\it es}$;${\it e'}$),$v$)))
\-\-\-\-
\end{tabbing}